(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #xCD93C5330A4D525D) #x4D93C5330A4D525D))
(constraint (= (f #xBE6143750510A683) #x3E6143750510A683))
(constraint (= (f #x89A7066D9178BA8E) #x09A7066D9178BA8F))
(constraint (= (f #x8A694D5D63202DC4) #x0A694D5D63202DC5))
(constraint (= (f #x9CF8647AD5018286) #x1CF8647AD5018287))
(constraint (= (f #xCA1A64B78F9E9E4D) #xF9AF2CDA43830B0D))
(constraint (= (f #xC5F8E096C54AEDFF) #xF9D038FB49D5A890))
(constraint (= (f #x0F357F8615CF7FE6) #xFF865403CF518400))
(constraint (= (f #x1A86307926FF1E3E) #xFF2BCE7C36C8070E))
(constraint (= (f #x4A2742BB626E53D4) #xFDAEC5EA24EC8D61))
(constraint (= (f #xE90F06B0A8095771) #x690F06B0A8095771))
(constraint (= (f #xD34484AA280190ED) #x534484AA280190ED))
(constraint (= (f #x3554822A2885D501) #x3554822A2885D501))
(constraint (= (f #xB35808A4C2011591) #x335808A4C2011591))
(constraint (= (f #xCC5002AA954102B7) #x4C5002AA954102B7))
(constraint (= (f #xFFFFFFFFFFFEA677) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFEAEC8) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFEA25B) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFE5700) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFECB76) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xF101845E0001FFFF) #x7101845E0001FFFF))
(constraint (= (f #x71CB06204883B719) #x71CB06204883B719))
(constraint (= (f #x09681690004FF891) #x09681690004FF891))
(constraint (= (f #x79D08600580FA5D1) #x79D08600580FA5D1))
(constraint (= (f #x1253A12054C32A3D) #x1253A12054C32A3D))
(check-synth)
